input-forwarding{i:l}
input-forwarding(es; Cmd; Sys; isupdate; In; f)
== e:E(Sys).
== (((e  In))  (Sys(e) = [In(e)]))
== & ((((e  In)))
== & ( ((loc(f(e)) = loc(e)))
== & ( (((e':E(Sys). ((e' <loc e) & loc(f(e')) = loc(f(e))))  (Sys(e) = Sys(f(e))))
== & ( & (((e':E(Sys). ((e' <loc e) & loc(f(e')) = loc(f(e)))))
== & ( & ( (Sys(e)
== & ( & ( (=
== & ( & ( (if e  prior(Sys)
== & ( & ( (then nth_tl(||filter(isupdate;es-interface-history(es; Sys; prior(Sys)(e)))||;
== & ( & ( (then nth_tl(filter(isupdate;es-interface-history(es; Sys; (f(e)))))
== & ( & ( (else filter(isupdate;es-interface-history(es; Sys; (f(e))))
== & ( & ( (fi ))))
== & ((((e  In)))  (loc(f(e)) = loc(e))  (Sys(e) = []))
== & (did-forward(es; Sys; f; e)
== & ( (a:E(Sys).
== & ( (a <loc e)  should-forward(es; In; isupdate; f; a)  did-forward(es; Sys; f; a))) 

latex

---

clarification:

input-forwarding{i:l}
input-forwarding(es; Cmd; Sys; isupdate; In; f)
== e:es-E-interface(es;Sys).
== (((e  In))  (Sys(e) = [In(e) / []]  (Cmd List)))
== & ((((e  In)))
== & ( ((es-loc(es; (f(e))) = es-loc(es; e)  Id))
== & ( (((e':es-E-interface(es;Sys)
== & ( ((((es-locl(es; e'; e) & es-loc(es; (f(e'))) = es-loc(es; (f(e)))  Id))
== & ( (( (Sys(e) = Sys(f(e))  (Cmd List)))
== & ( & (((e':es-E-interface(es;Sys)
== & ( & ((((es-locl(es; e'; e) & es-loc(es; (f(e'))) = es-loc(es; (f(e)))  Id)))
== & ( & ( (Sys(e)
== & ( & ( (=
== & ( & ( (if e  es-prior-interface{i:l}(es; Sys)
== & ( & ( (then nth_tl(||filter(isupdate
== & ( & ( (then nth_tl(||filter;es-interface-history(es;
== & ( & ( (then nth_tl(||filter;es-interface-history(Sys;
== & ( & ( (then nth_tl(||filter;es-interface-history(es-prior-interface{i:l}
== & ( & ( (then nth_tl(||filter;es-interface-history(es-prior-interface(es; Sys)(e)))||;
== & ( & ( (then nth_tl(filter(isupdate;es-interface-history(es; Sys; (f(e)))))
== & ( & ( (else filter(isupdate;es-interface-history(es; Sys; (f(e))))
== & ( & ( (fi 
== & ( & ( ( (Cmd List)))))
== & ((((e  In)))  (es-loc(es; (f(e))) = es-loc(es; e)  Id)  (Sys(e) = []  (Cmd List)))
== & (did-forward(es; Sys; f; e)
== & ( (a:es-E-interface(es;Sys).
== & ( es-locl(es; a; e)
== & (  should-forward(es; In; isupdate; f; a)
== & (  did-forward(es; Sys; f; a))) 

latex

Up	abstract chain replication
Wellformedness Lemmas	input-forwarding wf
Definitions	[car / cdr], x:A. B(x), P & Q, if b then t else f fi , nth_tl(n;as), ||as||, prior(X), filter(P;l), es-interface-history(es; X; e), A, b, e  X, Id, f(a), loc(e), s = t, type List, X(e), [], x:A. B(x), E(X), (e <loc e'), P  Q, should-forward(es; In; isupdate; f; a), did-forward(es; Sys; f; e)
FDL editor aliases	input-forwarding